ecl{-}halt{-}kind($x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind($x$;$k$,${\it test}$.inl $k$ ;$a$,$b$,${\it ha}$,${\it hb}$.${\it hb}$;$a$,$b$,${\it ha}$,${\it hb}$.inr $\cdot$ ;$a$,$b$,${\it ha}$,${\it hb}$.inr $\cdot$ ;$a$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.${\it ha}$;$a$,$l$,${\it ha}$.inr $\cdot$ )